/*******************************************************************************
 * Copyright (c) 2009 Kevin Bierhoff and others.
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *     Kevin Bierhoff - initial API and implementation
 *******************************************************************************/
package com.googlecode.twelfdevtools.twelfast;

import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.Reader;
import java.io.StringReader;
import java.util.List;

import com.googlecode.twelfdevtools.model.IDeclarationContext;
import com.googlecode.twelfdevtools.model.ITwelfConstant;
import com.googlecode.twelfdevtools.twelfparser.TwelfLexer;
import com.googlecode.twelfdevtools.twelfparser.TwelfParser;



import antlr.RecognitionException;
import antlr.TokenStreamException;

public class TwelfAST {
	
	public static List<ITwelfDeclaration> parseElfCode(String code) 
	throws RecognitionException, TokenStreamException {
		return parseElfFile(new StringReader(code));
	}
	
	public static List<ITwelfDeclaration> parseElfFile(InputStream source) 
	throws RecognitionException, TokenStreamException {
		return parseElfFile(new InputStreamReader(source));
	}
	
	public static List<ITwelfDeclaration> parseElfFile(Reader source) 
	throws RecognitionException, TokenStreamException {
		try {
			TwelfLexer l = new TwelfLexer(source);
			TwelfParser p = new TwelfParser(l);
			return p.startRule();
		}
		finally {
			try {
				source.close();
			}
			catch(IOException e) {
				e.printStackTrace();
			}
		}
	}

	private static ITwelfDeclaration parseTwelfDeclaration(String code) 
	throws RecognitionException, TokenStreamException {
		return parseTwelfDeclaration(new StringReader(code), 0, 0);
	}

	public static ITwelfDeclaration parseTwelfDeclaration(String code, int line, int col) 
	throws RecognitionException, TokenStreamException {
		return parseTwelfDeclaration(new StringReader(code), line, col);
	}

	/** 
	 * Parse the given Twelf declaration, assuming the given 
	 * <b>0-based</b> start position in a (hypothetical) file. 
	 */
	public static ITwelfDeclaration parseTwelfDeclaration(Reader source, int line, int col)
	throws RecognitionException, TokenStreamException {
		try {
			TwelfLexer l = new TwelfLexer(source);
			// set start position in lexer
			// Antlr uses 1-based rows and columns!
			l.setLine(line+1); l.setColumn(col+1);
			TwelfParser p = new TwelfParser(l);
			return p.decl();
		}
		finally {
			try {
				source.close();
			}
			catch(IOException e) {
				e.printStackTrace();
			}
		}
	}

	/** Find the identifier at the given <b>0-based</b> row and column. */
	public static ITwelfIdentifier findIdentifier(ITwelfAstNode node,
			int line, int column) {
		// Antlr uses 1-based rows and columns!
		return new FindIdVisitor(line+1, column+1).doDispatch(node);
	}
	
	public static void bind(ITwelfDeclaration decl, ITwelfConstant declModel,
			final IDeclarationContext ctx) throws RecognitionException, TokenStreamException {
		ITwelfDeclaration explicitDecl = 
			parseTwelfDeclaration(declModel.getDeclaration() + ".");
		
		bind(explicitDecl, new ITwelfTermContext() {

			public ITwelfBinding getBinding(String id) {
				ITwelfConstant c = ctx.getConstant(id);
				if(c == null)
					return null;
				else
					return new ConstantBinding(c);
			}
			
		}, declModel);
		
		sync(decl, explicitDecl);
	}

	private static void sync(ITwelfDeclaration decl,
			ITwelfDeclaration explicitDecl) {
		explicitDecl.dispatch(new Sync(decl));
	}

	/**
	 * Only call this method for <i>explicit</i>, i.e., fully expanded Twelf
	 * terms as they are output by the Twelf server.
	 * @param explicitNode
	 * @param context
	 */
	static void bind(ITwelfAstNode explicitNode,
			ITwelfTermContext context, ITwelfConstant constant) {
		explicitNode.dispatch(new Binder(context, constant));
	}

	private static class FindIdVisitor extends AbstractTwelfAstVisitor<ITwelfIdentifier>
	implements ITwelfAstVisitor<ITwelfIdentifier> {

		private int line;
		private int column;

		public FindIdVisitor(int line, int column) {
			this.line = line;
			this.column = column;
		}
		
		private ITwelfIdentifier checkIdentifier(ITwelfIdentifier node) {
			if(node.getStartRow() == line && node.getStartColumn() <= column &&
					(line < node.getEndRow() || column < node.getEndColumn()))
				return node;
			if(node.getStartRow() < line && 
					(line < node.getEndRow() || 
							(line == node.getEndRow() && column < node.getEndColumn())))
				return node;
			return null;
		}

		public ITwelfIdentifier app(Application node) {
			ITwelfIdentifier result = doDispatch(node.getLhs());
			if(result == null)
				result = doDispatch(node.getRhs());
			return result;
		}

		public ITwelfIdentifier arrow(Arrow node) {
			ITwelfIdentifier result = doDispatch(node.getLhs());
			if(result == null)
				result = doDispatch(node.getRhs());
			return result;
		}

		public ITwelfIdentifier ascr(Ascription node) {
			ITwelfIdentifier result = doDispatch(node.getTerm());
			if(result == null)
				result = doDispatch(node.getAscription());
			return result;
		}

		public ITwelfIdentifier constDecl(ConstantDeclaration node) {
			ITwelfIdentifier result = doDispatch(node.getConst());
			if(result == null)
				result = doDispatch(node.getTerm());
			if(result == null)
				result = doDispatch(node.getValue());
			return result;
		}

		public ITwelfIdentifier lambda(Lambda node) {
			ITwelfIdentifier result = doDispatch(node.getId());
			if(result == null)
				result = doDispatch(node.getIdTerm());
			if(result == null)
				result = doDispatch(node.getTerm());
			return result;
		}

		public ITwelfIdentifier pi(Pi node) {
			ITwelfIdentifier result = doDispatch(node.getId());
			if(result == null)
				result = doDispatch(node.getIdTerm());
			if(result == null)
				result = doDispatch(node.getTerm());
			return result;
		}

		public ITwelfIdentifier type(Type node) {
			return null; // "type" is not an identifier
		}

		public ITwelfIdentifier id(Identifier node) {
			return checkIdentifier(node);
		}

		public ITwelfIdentifier wildcard(Wildcard node) {
			return checkIdentifier(node);
		}
		
	}

}
